$\forall$$T$, ${\it T'}$:Type, $x$:Id, $c$:$T$, $a$:Id, $P$:($T$$\rightarrow$${\it T'}$$\rightarrow$Prop).
\\[0ex]ma{-}single{-}pre{-}init1($x$;$T$;$c$;$a$;${\it T'}$;$x$,$v$.$P$($x$,$v$)) $\in$ MsgA